RCS "$Id: AgentProtected.sig,v 1.12 1998/08/13 11:37:59 pxs Exp $";
(* See Agent.sig. This is the more permissive version of that. *)
signature AGENT_PROTECTED =
sig
  include AGENT
    
   structure A'  : ACT_PROTECTED sharing A = A'
   structure Eval : EVAL sharing A'.Value' = Eval.Value
   structure P : PREFIX sharing P.A = A'

   type literalRelabelling

   datatype param = ActParam   of A'.act
(* I hate ML. See below. *)
   | ActionSetParam of A'.ActionSet.set MaybeVar.maybeVar (* actionSet *)
   | TimeParam  of int
   | AgentParam of agent

        and privateAgent = Nil
                  | DNil
                  | Bottom
                  | Var      of V.var * param list
                  | Prefix   of P.prefix list * agent
                  | Delta    of P.prefix * agent
                  | Time     of int * agent
                  | WSum     of agent list
                  | SSum     of agent list
                  | Parallel of agent list
                  | SMerge   of (agent * A'.ActionSet.set MaybeVar.maybeVar) list
(* I can't work out how to share type t = s list etc. or I'd do this  *)
(* differently... *)
                  | Restrict of agent * (A'.PortSet.set MaybeVar.maybeVar)
                  | Relabel  of agent * (literalRelabelling MaybeVar.maybeVar)
	          | Open     of agent * Eval.evaluation
(* NOTHING, but NOTHING, should use this directly. Use real and hashval *)
(* Does ML really force me to put it here? *)
   and agent' = DUMMY of (privateAgent * Word.word) ref
     sharing type agent = agent'

   val real : agent -> privateAgent
   val makeAgent : privateAgent -> agent
   val relabelWithList : agent * (A'.act * A'.act) list -> agent
   val relabelWithVar : agent * V.var -> agent
    
(* stuff needed in Extra *)
   val lookupAgent : V.var -> (param list * agent) option
   val getAgentFPs : param list -> V.var list
   val mksubst : param list -> param list ->
     ((A'.act -> int) * (A'.act -> A'.act) *
      (V.var -> (A'.ActionSet.set MaybeVar.maybeVar)) * (agent -> agent))
   val apply : V.var list ->
     ((A'.act -> int) * (A'.act -> A'.act) *
      (V.var -> (A'.ActionSet.set MaybeVar.maybeVar)) * (agent -> agent)) ->
     agent -> agent
   val dumbActionFromPrefix : P.prefix -> A'.act
   val set_lookup : A'.ActionSet.set MaybeVar.maybeVar -> A'.ActionSet.set
   val rel_lookup : literalRelabelling MaybeVar.maybeVar -> literalRelabelling
   val restrictionLookup : A'.PortSet.set MaybeVar.maybeVar -> A'.PortSet.set
   val O : literalRelabelling * literalRelabelling -> literalRelabelling
   val relabel : agent * literalRelabelling -> agent
   val forbids : A'.PortSet.set -> A'.act -> bool
   val relabelAction : literalRelabelling -> A'.act -> A'.act
   val makeLiteralRelabelling : (A'.act * A'.act) list -> literalRelabelling

(* Things reading two args expect (first,second). *)
    val readNatAgent : unit -> (int * agent)
(* eps isn't allowed *)
    val readActAgent : unit -> (A.act * agent)
(* (a,b,...,A) -- for historical reasons! Must have at least one action. *)
(* bool is whether eps and taus are allowed *)
    val readActlistAgent : bool -> (A.act list * agent)
(* [a/b,...,y/z], maybe empty, eps not allowed as 1st, eps nor tau as 2nd *)
    val readRelabelling : unit -> (A.act * A.act) list

    val setmkstr : ('a -> string) -> 'a list -> string
    val actseq : A.act list -> string
      
    val agent2whatever : ('a -> string) -> (agent -> 'a) -> (unit -> unit)
    val agent2agent : (agent -> agent) -> (unit -> unit)
    val agent2bool : (agent -> bool) -> (unit -> unit)
end

